#include "FreeRTOS.h"
#include "queue.h"
#include "queue_datastructure.h"

/* Using prvCopyDataToQueue together with prvNotifyQueueSetContainer
   leads to a problem space explosion. Therefore, we use this stub
   and a sepearted proof on prvCopyDataToQueue to deal with it.
   As prvNotifyQueueSetContainer is disabled if configUSE_QUEUE_SETS != 1,
   in other cases the original implementation should be used. */
#if( configUSE_QUEUE_SETS == 1 )
	BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition )
	{
		if(pxQueue->uxItemSize > ( UBaseType_t ) 0)
		{
			__CPROVER_assert(__CPROVER_r_ok(pvItemToQueue, ( size_t ) pxQueue->uxItemSize), "pvItemToQueue region must be readable");
			if(xPosition == queueSEND_TO_BACK){
				__CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->pcWriteTo, ( size_t ) pxQueue->uxItemSize), "pxQueue->pcWriteTo region must be writable");
			}else{
				__CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize), "pxQueue->u.xQueue.pcReadFrom region must be writable");
			}
			return pdFALSE;
		}else
		{
			return nondet_BaseType_t();
		}
	}
#endif

/* xQueueCreateSet is compiled out if configUSE_QUEUE_SETS != 1.*/
#if( configUSE_QUEUE_SETS == 1 )
	QueueSetHandle_t xUnconstrainedQueueSet()
	{
		UBaseType_t uxEventQueueLength = 2;
		QueueSetHandle_t xSet = xQueueCreateSet(uxEventQueueLength);
		if( xSet )
		{
			xSet->cTxLock = nondet_int8_t();
			xSet->cRxLock = nondet_int8_t();
			xSet->uxMessagesWaiting = nondet_UBaseType_t();
			xSet->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
			/* This is an invariant checked with a couple of asserts in the code base.
			   If it is false from the beginning, the CBMC proofs are not able to succeed*/
			__CPROVER_assume(xSet->uxMessagesWaiting < xSet->uxLength);
			xSet->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();
		}
		return xSet;
	}
#endif

/* Create a mostly unconstrained Queue but bound the max item size.
   This is required for performance reasons in CBMC at the moment. */
QueueHandle_t xUnconstrainedQueueBoundedItemSize( UBaseType_t uxItemSizeBound ) {
	UBaseType_t uxQueueLength;
	UBaseType_t uxItemSize;
	uint8_t ucQueueType;
	__CPROVER_assume(uxQueueLength > 0);
	__CPROVER_assume(uxItemSize < uxItemSizeBound);
	/* The implicit assumption for the QueueGenericCreate method is,
	   that there are no overflows in the computation and the inputs are safe.
	   There is no check for this in the code base */
	UBaseType_t upper_bound = portMAX_DELAY - sizeof(Queue_t);
	__CPROVER_assume(uxItemSize < (upper_bound)/uxQueueLength);
	QueueHandle_t xQueue =
		xQueueGenericCreate(uxQueueLength, uxItemSize, ucQueueType);
	if(xQueue){
		xQueue->cTxLock = nondet_int8_t();
		xQueue->cRxLock = nondet_int8_t();
		xQueue->uxMessagesWaiting = nondet_UBaseType_t();
		/* This is an invariant checked with a couple of asserts in the code base.
		   If it is false from the beginning, the CBMC proofs are not able to succeed*/
		__CPROVER_assume(xQueue->uxMessagesWaiting < xQueue->uxLength);
		xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
		xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();
		#if( configUSE_QUEUE_SETS == 1)
			xQueueAddToSet(xQueue, xUnconstrainedQueueSet());
		#endif
	}
	return xQueue;
}

/* Create a mostly unconstrained Queue */
QueueHandle_t xUnconstrainedQueue( void ) {
	UBaseType_t uxQueueLength;
	UBaseType_t uxItemSize;
	uint8_t ucQueueType;
	__CPROVER_assume(uxQueueLength > 0);
	/* The implicit assumption for the QueueGenericCreate method is,
	   that there are no overflows in the computation and the inputs are safe.
	   There is no check for this in the code base */
	UBaseType_t upper_bound = portMAX_DELAY - sizeof(Queue_t);
	__CPROVER_assume(uxItemSize < (upper_bound)/uxQueueLength);
	QueueHandle_t xQueue =
		xQueueGenericCreate(uxQueueLength, uxItemSize, ucQueueType);
	if(xQueue){
		xQueue->cTxLock = nondet_int8_t();
		xQueue->cRxLock = nondet_int8_t();
		xQueue->uxMessagesWaiting = nondet_UBaseType_t();
		/* This is an invariant checked with a couple of asserts in the code base.
		   If it is false from the beginning, the CBMC proofs are not able to succeed*/
		__CPROVER_assume(xQueue->uxMessagesWaiting < xQueue->uxLength);
		xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
		xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();
		#if( configUSE_QUEUE_SETS == 1)
			xQueueAddToSet(xQueue, xUnconstrainedQueueSet());
		#endif
	}
	return xQueue;
}

/* Create a mostly unconstrained Mutex */
QueueHandle_t xUnconstrainedMutex( void ) {
	uint8_t ucQueueType;
	QueueHandle_t xQueue =
		xQueueCreateMutex(ucQueueType);
	if(xQueue){
		xQueue->cTxLock = nondet_int8_t();
		xQueue->cRxLock = nondet_int8_t();
		xQueue->uxMessagesWaiting = nondet_UBaseType_t();
		/* This is an invariant checked with a couple of asserts in the code base.
		   If it is false from the beginning, the CBMC proofs are not able to succeed*/
		__CPROVER_assume(xQueue->uxMessagesWaiting < xQueue->uxLength);
		xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
		xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();
		#if( configUSE_QUEUE_SETS == 1)
			xQueueAddToSet(xQueue, xUnconstrainedQueueSet());
		#endif
	}
	return xQueue;
}
